E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), pred?:(E(E+Unit)).
SWellFounded(pred!(e;e'))
 (e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 (e, e':E. loc(e) = loc(e')  Id  pred?(e) = pred?(e')  e = e')
 (e, e':E. loc(e) = loc(e')  Id  e < e'  (e x,y. first(y) & x = pred(y)  E^+ e')) 

latex

Definitions	Trans x,y:T. E(x;y), R1 => R2, x. t(x), P  Q, P  Q, rcv?(e), sender(e), A & B, {T}, x f y, R^+, e < e', b, first(e), Prop, pred(e), loc(e), SWellFounded(R(x;y)), x,y. t(x;y), pred!(e;e'), Unit, Id, IdLnk, t  T, x:A. B(x), A, False, P  Q, WellFnd{i}(A;x,y.R(x;y))
Lemmas	pred-total, IdLnk wf, Id wf, unit wf, pred! wf, strongwellfounded wf, loc wf, pred wf, first wf, assert wf, not wf, cless wf, wellfounded functionality wrt implies, strongwf-implies, sender wf, rcv? wf, rel plus strongwellfounded, rel plus monotone, rel plus trans